Лестница в HoTT: лямбда история

FROM: Максим Сохацкий
TO: Формальная Философия

Здесь будет представлена глубокая и обширная история логики и формальной математики, которую я когда-то увидел на слайдах Даны Скотта в 2012 году. Лестниц в HoTT есть много. Как говорят в буддизме "для существ с высокими способностями", достатоточно учебника HoTT, чтобы понять всё сразу. Для существ со средними способностями достаточно покрутить лямбда куб и пойти по Барендрехту. Для существ с низкими способностями, как я, предлагаю ознакомиться с путем Дана Скотта, т.е. наиболее детальным и длинным, который пришлось пройти и мне.

Сам же я сторонник краткого учебника, который можно усилить даже интерпретатором, тайпчекером и своей вариацией HoTT, которую представляют собой практически все HoTT курсы, включая курс Роберта Харпера 15-819.

Если спросить о моем таком курсе, для существ с высшими способностями, то он пока не сформирован в учебник, но несколько глав для ознакомления можно посмотреть тут, а мой список литературы, являющийся частью этого (расширеного) списка Даны Скотта, для существ со средними способностями состоящий из 60 работ можно найти тут. Понятное дело, что это все для программистов!

1870-е

Begriffsschrift: Frege (1879)

1880-е

What are numbers?: Dedekind (1888)
Number-theoretic axioms: Peano (1889)

1890-е

Vorlesungen über die Algebra der Logik: Schröder (1890–1905)
Grundgesetze der Arithmetik: Frege (1893-1903)
Formulario Mathematico: Peano (1895-1901)
Grundlagen der Geometrie: Hilbert (1899)

1900-е

Diophantine problem: Hilbert (1900)
Russell's Paradox: Russell (1901)
Principles of Mathematics: Russell (1903)
Richard’s Paradox: Richard (1905)
Theory of Types: Russell (1908)

1910-е

Principia Mathematica: Whitehead-Russell (1910-12-13)
Calculus of relatives: Löwenheim (1915)

1920-е

Löwenheim-Skolem Theorem: Skolem (1920)
Propositional calculus completeness: Post (1921)
Monadic predicate calculus decidable: Behmann (1922)
Abstract proof rules: Hertz (1922)
Primitive recursive arithmetic: Skolem (1923)
Combinators: Schönfinkel (1924)
Function-based set theory: Vvon Neumann (1925)
“Conceptual” undecidability: Finsler (1926)
Epsilon operator: Hilbert-Bernays (1927)
Combinators (again): Curry (1927)
Ackermann function: Ackermann (1928)
Entscheidungsproblem: Hilbert-Ackermann (1928)
Abriss der Logistik & simple type theory: Carnap (1929)

1930-е

Combinatory logic: Curry (1930-32)
Herbrand’s Theorem: Herbrand (1930)
Completeness proof: Gödel (1930)
Partial consistency proof: Herbrand (1931)
Incompleteness: Gödel (1931)
Untyped λ-calculus: Church (1932-33-41)
Studies of primitive recursion: Péter (1932-36)
Non-standard models: Skolem (1933)
Functionality in Combinatory Logic: Curry (1934)
Grundlagen der Mathematik: Hilbert-Bernays (1934-39)
Natural deduction: Gentzen (1934)
Number-theoretic consistency & 0-induction: Gentzen (1934)
Inconsistency of Church’s System: Kleene-Rosser (1936)
Confluence theorem: Church-Rosser (1936)
Finite combinatory processes: Post (1936)
Turing machines: Turing (1936-37)
Recursive undecidability: Church-Turing (1936)
General recursive functions: Kleene (1936)
Further completeness proofs: Maltsev (1936)
Improving incompleteness theorems: Rosser (1936)
Fixed-point combinator: Turing (1937)
Computability and λ-definability: Turing (1937)

1940-е

Simple type theory & λ-calculus: Church (1940)
Primitive recursive functionals: Gödel (1941-58)
Recursive hierarchies: Kleene (1943)
Theory of categories: Eilenberg-Mac Lane (1945)
New completeness proofs: Henkin (1949-50)

1950-е

Computing and Intelligence: Turing (1950)
Rethinking combinators: Rosenbloom (1950)
Introduction to Metamathematics: Kleene (1952)
Arithmetical predicates: Kleene (1955)
Combinatory Logic. Volume I.: Curry-Feys-Craig (1958)
Adjoint functors: Kan (1958)
Recursive functionals & quantifiers, I.&II.: Kleene (1959-63)
Countable functionals: Kleene-Kreisel (1959)

1960-е

Elementary formal systems: Smullyan (1961)
Grothendieck Topologies: M.Artin (1962)
Higher-type λ-definability: Kleene (1962)
Grothendieck topoi: Grothendieck et al. SGA 4 (1963-64-72)
Functorial semantics: Lawvere (1963)
Adjoint functors & triples: Eilenberg-Moore (1965)
Cartesian closed categories: Eilenberg-Kelly (1966)
New foundations of recursion theory: Platek (1966)
Normalization Theorem: Tait (1967)
AUTOMATH & dependent types: de Bruijn (1967)
Finite-type computable functionals: Gandy (1967)
Normal-form discrimination: Böhm (1968)
Category of sets: Lawvere (1969)
Typed domain logic: Scott (1969-93)
Domain-theoretic λ-models: Scott (1969)
Formulae-as-types: Howard (1969 -1980)
Adjointness in foundations: Lawvere (1969)

1970-е

Categorical logic: Joyal (1970+)
Elementary topoi: Lawvere-Tierney (1970)
Denotational semantics: Scott-Strachey (1970)
Coherence in closed categories: Kelly (1971)
Quantifiers and sheaves: Lawvere (1971)
Martin-Löf type theory: Martin-Löf (1971)
System F, Fω: Girard (1971)
Logic for Computable Functions: Milner (1972)
From sheaves to logic: Reyes (1974)
Polymorphic λ-calculus: Reynolds (1974)
Call-by-name, call-by-value: Plotkin (1975)
Modeling Processes: Milner (1975)
SASL: Turner (1975)
Scheme: Sussman-Steele (1975-80)
Functional programming & FP: Backus (1977)
First-order categorical logic: Makkai-Reyes (1977)
Edinburgh LCF: Milner et al. (1978)
Let-polymorphic type inference: Milner (1978)
Intersection types: Coppo-Dezani (1978)
ML: Milner et al. (1979)
*-Autonomous categories: Barr (1979)
Sheaves and logic: Fourman-Scott (1979)

1980-е

Frege structures: Aczel (1980)
HOPE: Burstall et al. (1980)
The Lambda Calculus Book: Barendregt (1981-84)
Structural Operational Semantics: Plotkin (1981)
Effective Topos: Hyland (1982)
Dependent types & modularity: Burstall-Lampson (1984)
Locally CCC & type theory: R.A.G. Seely (1984)
Calculus of Constructions: Coquand-Huet (1985)
Bounded quantification: Cardelli-Wegner (1985)
NUPRL: Constable et al. (1986)
Higher-order categorical logic: Lambek-P.J.Scott (1986)
Cambridge LCF: Paulson (1987)
Linear logic: Girard et al. (1987-89)
HOL: Gordon (1988)
FORSYTHE: Reynolds (1988)
Proofs and Types: Girard et al. (1989)
Integrating logical & categorical types: Gray (1989)
Computational λ-calculus & monads: Moggi (1989)

1990-е

Haskell: Hudak-Hughes-Peyton Jones-Wadler (1990)
Higher-type recursion theory: Sacks (1990)
Standard ML: Milner, et al. (1990-97)
Lazy λ-calculus: Abramsky (1990)
Higher-order subtyping: Cardelli-Longo (1991)
Categories, Types and Structure: Asperti-Longo (1991)
STANDARD ML of NJ: MacQueen-Appel (1991-98)
QUEST: Cardelli (1991)
Edinburgh LF: Harper, et al. (1992)
Pi-Calculus: Milner-Parrow-Walker (1992)
Categorical combinators: Curien (1993)
Translucent types & modular: Harper-Lillibridge (1994)
Full abstraction for PCF: Hyland-Ong/Abramsky, et al. (1995)
Algebraic set theory: Joyal-Moerdijk (1995)
Object Calculus: Abadi-Cardelli (1996)
Typed intermediate languages: Tarditi, Morrisett, et al. (1996)
Proof-carrying code: Necula-Lee (1996)
Computability and totality in domains: Berger (1997)
Typed assembly language: Morrisett, et al. (1998)
Type theory via exact categories: Birkedal, et al. (1998)
Categorification: Baez (1998)

2000-е

Predicative topos: Moerdijk-Palmgren (2000)
Sketches of an Elephant: Johnstone (2002+)
Differential λ-calculus: Ehrhard/Regnier (2003)
Modular Structural Operational Semantics: Mosses (2004)
A λ-calculus for real analysis: Taylor (2005+)
Homotopy type theory: Awodey-Warren (2006)
Univalence axiom: Voevodsky (2006+)
The safe λ-calculus: Ong, et al. (2007)
Higher topos theory: Lurie (2009)

2010-е

Functional Reactive Programming: Hudak, et al. (2010)
HoTT Book: Voevodsky, et al. (2012-13)